A:Type, R:(ARealizer), i:Id, L:(A List).
(R-has-loc(xL.R(x);i))  (xL.R-has-loc(R(x);i)) 

latex

Definitions	{T}, P  Q, , S  T, P  Q, P  Q, P & Q, if b then t else f fi , Y, x. t(x), t  T, Top, ff, reduce(f;k;as), x(s), b, P  Q, x:A. B(x), False
Lemmas	assert of bor, l exists cons, l exists nil, iff functionality wrt iff, bfalse wf, bool wf, reduce wf, bor wf, R-has-loc wf, assert wf, l exists wf, false wf, es realizer wf, Id wf, top wf, Rall-has-loc